Runtime Complexity (innermost) proof of /tmp/tmppiMhJT/gexgcd2.xml

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2).

0 CpxRelTRS

↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)

↳2 CpxTRS

↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 7 ms)

↳4 CdtProblem

↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CdtProblem

↳9 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳10 CdtProblem

↳11 CdtUsableRulesProof (⇔, 0 ms)

↳12 CdtProblem

↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 176 ms)

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 56 ms)

↳16 CdtProblem

↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 54 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 230 ms)

↳20 CdtProblem

↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳22 CdtProblem

↳23 CdtUsableRulesProof (⇔, 0 ms)

↳24 CdtProblem

↳25 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳26 CdtProblem

↳27 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳28 CdtProblem

↳29 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 1 ms)

↳30 CdtProblem

↳31 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 26 ms)

↳32 CdtProblem

↳33 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 624 ms)

↳34 CdtProblem

↳35 CdtKnowledgeProof (⇔, 0 ms)

↳36 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

monus(S(x'), S(x)) → monus(x', x)
gcd(x, y) → gcd[Ite](equal0(x, y), x, y)
equal0(a, b) → equal0[Ite](<(a, b), a, b)

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
gcd[Ite](False, x, y) → gcd[False][Ite](<(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(y, monus(y, x))
gcd[False][Ite](True, x, y) → gcd(monus(x, y), y)
equal0[Ite](False, a, b) → False
equal0[Ite](True, a, b) → equal0[True][Ite](<(b, a), a, b)
equal0[True][Ite](False, a, b) → False
equal0[True][Ite](True, a, b) → True

Rewrite Strategy: INNERMOST

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

monus(S(x'), S(x)) → monus(x', x)
gcd(x, y) → gcd[Ite](equal0(x, y), x, y)
equal0(a, b) → equal0[Ite](<(a, b), a, b)
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
gcd[Ite](False, x, y) → gcd[False][Ite](<(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(y, monus(y, x))
gcd[False][Ite](True, x, y) → gcd(monus(x, y), y)
equal0[Ite](False, a, b) → False
equal0[Ite](True, a, b) → equal0[True][Ite](<(b, a), a, b)
equal0[True][Ite](False, a, b) → False
equal0[True][Ite](True, a, b) → True

Rewrite Strategy: INNERMOST

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

monus(S(z0), S(z1)) → monus(z0, z1)
gcd(z0, z1) → gcd[Ite](equal0(z0, z1), z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
gcd[Ite](False, z0, z1) → gcd[False][Ite](<(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) → z0
gcd[False][Ite](False, z0, z1) → gcd(z1, monus(z1, z0))
gcd[False][Ite](True, z0, z1) → gcd(monus(z0, z1), z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c2(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
<'(0, S(z0)) → c4
<'(z0, 0) → c5
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[ITE](True, z0, z1) → c7
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](False, z0, z1) → c10
EQUAL0[ITE](True, z0, z1) → c11(EQUAL0[TRUE][ITE](<(z1, z0), z0, z1), <'(z1, z0))
EQUAL0[TRUE][ITE](False, z0, z1) → c12
EQUAL0[TRUE][ITE](True, z0, z1) → c13

S tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c2(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
<'(0, S(z0)) → c4
<'(z0, 0) → c5
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[ITE](True, z0, z1) → c7
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](False, z0, z1) → c10
EQUAL0[ITE](True, z0, z1) → c11(EQUAL0[TRUE][ITE](<(z1, z0), z0, z1), <'(z1, z0))
EQUAL0[TRUE][ITE](False, z0, z1) → c12
EQUAL0[TRUE][ITE](True, z0, z1) → c13

K tuples:none
Defined Rule Symbols:

monus, gcd, equal0, <, gcd[Ite], gcd[False][Ite], equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

MONUS, GCD, EQUAL0, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0[TRUE][ITE]

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 6 trailing nodes:

EQUAL0[TRUE][ITE](True, z0, z1) → c13
<'(z0, 0) → c5
GCD[ITE](True, z0, z1) → c7
EQUAL0[TRUE][ITE](False, z0, z1) → c12
<'(0, S(z0)) → c4
EQUAL0[ITE](False, z0, z1) → c10

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

monus(S(z0), S(z1)) → monus(z0, z1)
gcd(z0, z1) → gcd[Ite](equal0(z0, z1), z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
gcd[Ite](False, z0, z1) → gcd[False][Ite](<(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) → z0
gcd[False][Ite](False, z0, z1) → gcd(z1, monus(z1, z0))
gcd[False][Ite](True, z0, z1) → gcd(monus(z0, z1), z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c2(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(EQUAL0[TRUE][ITE](<(z1, z0), z0, z1), <'(z1, z0))

S tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c2(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(EQUAL0[TRUE][ITE](<(z1, z0), z0, z1), <'(z1, z0))

K tuples:none
Defined Rule Symbols:

monus, gcd, equal0, <, gcd[Ite], gcd[False][Ite], equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

MONUS, GCD, EQUAL0, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE]

Compound Symbols:

c, c1, c2, c3, c6, c8, c9, c11

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

monus(S(z0), S(z1)) → monus(z0, z1)
gcd(z0, z1) → gcd[Ite](equal0(z0, z1), z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
gcd[Ite](False, z0, z1) → gcd[False][Ite](<(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) → z0
gcd[False][Ite](False, z0, z1) → gcd(z1, monus(z1, z0))
gcd[False][Ite](True, z0, z1) → gcd(monus(z0, z1), z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c2(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))

S tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
EQUAL0(z0, z1) → c2(EQUAL0[ITE](<(z0, z1), z0, z1), <'(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))

K tuples:none
Defined Rule Symbols:

monus, gcd, equal0, <, gcd[Ite], gcd[False][Ite], equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

MONUS, GCD, EQUAL0, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE]

Compound Symbols:

c, c1, c2, c3, c6, c8, c9, c11

(9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

monus(S(z0), S(z1)) → monus(z0, z1)
gcd(z0, z1) → gcd[Ite](equal0(z0, z1), z0, z1)
equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
gcd[Ite](False, z0, z1) → gcd[False][Ite](<(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) → z0
gcd[False][Ite](False, z0, z1) → gcd(z1, monus(z1, z0))
gcd[False][Ite](True, z0, z1) → gcd(monus(z0, z1), z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

S tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

K tuples:none
Defined Rule Symbols:

monus, gcd, equal0, <, gcd[Ite], gcd[False][Ite], equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

MONUS, GCD, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0

Compound Symbols:

c, c1, c3, c6, c8, c9, c11, c4

(11) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

gcd(z0, z1) → gcd[Ite](equal0(z0, z1), z0, z1)
gcd[Ite](False, z0, z1) → gcd[False][Ite](<(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) → z0
gcd[False][Ite](False, z0, z1) → gcd(z1, monus(z1, z0))
gcd[False][Ite](True, z0, z1) → gcd(monus(z0, z1), z1)

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True
monus(S(z0), S(z1)) → monus(z0, z1)

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

S tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

K tuples:none
Defined Rule Symbols:

equal0, equal0[Ite], <, equal0[True][Ite], monus

Defined Pair Symbols:

MONUS, GCD, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0

Compound Symbols:

c, c1, c3, c6, c8, c9, c11, c4

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))

We considered the (Usable) Rules:

monus(S(z0), S(z1)) → monus(z0, z1)

And the Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(<(x₁, x₂)) = 0
POL(<'(x₁, x₂)) = 0
POL(EQUAL0(x₁, x₂)) = 0
POL(EQUAL0[ITE](x₁, x₂, x₃)) = 0
POL(False) = [2]
POL(GCD(x₁, x₂)) = x₁ + [2]x₂
POL(GCD[FALSE][ITE](x₁, x₂, x₃)) = x₂ + [2]x₃
POL(GCD[ITE](x₁, x₂, x₃)) = x₂ + [2]x₃
POL(MONUS(x₁, x₂)) = x₁
POL(S(x₁)) = [2] + x₁
POL(True) = 0
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁, x₂)) = x₁ + x₂
POL(equal0(x₁, x₂)) = [3] + [3]x₁
POL(equal0[Ite](x₁, x₂, x₃)) = [2]
POL(equal0[True][Ite](x₁, x₂, x₃)) = [2]x₁
POL(monus(x₁, x₂)) = 0

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True
monus(S(z0), S(z1)) → monus(z0, z1)

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

S tuples:

GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))

Defined Rule Symbols:

equal0, equal0[Ite], <, equal0[True][Ite], monus

Defined Pair Symbols:

MONUS, GCD, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0

Compound Symbols:

c, c1, c3, c6, c8, c9, c11, c4

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))

We considered the (Usable) Rules:

<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
<(0, S(z0)) → True
<(S(z0), S(z1)) → <(z0, z1)

And the Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(<(x₁, x₂)) = x₁
POL(<'(x₁, x₂)) = 0
POL(EQUAL0(x₁, x₂)) = x₁
POL(EQUAL0[ITE](x₁, x₂, x₃)) = x₁
POL(False) = 0
POL(GCD(x₁, x₂)) = x₁ + x₂
POL(GCD[FALSE][ITE](x₁, x₂, x₃)) = x₃
POL(GCD[ITE](x₁, x₂, x₃)) = x₃
POL(MONUS(x₁, x₂)) = 0
POL(S(x₁)) = x₁
POL(True) = [1]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁, x₂)) = x₁ + x₂
POL(equal0(x₁, x₂)) = 0
POL(equal0[Ite](x₁, x₂, x₃)) = 0
POL(equal0[True][Ite](x₁, x₂, x₃)) = 0
POL(monus(x₁, x₂)) = 0

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True
monus(S(z0), S(z1)) → monus(z0, z1)

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

S tuples:

GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))

Defined Rule Symbols:

equal0, equal0[Ite], <, equal0[True][Ite], monus

Defined Pair Symbols:

MONUS, GCD, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0

Compound Symbols:

c, c1, c3, c6, c8, c9, c11, c4

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))

We considered the (Usable) Rules:

<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
<(0, S(z0)) → True
<(S(z0), S(z1)) → <(z0, z1)

And the Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(<(x₁, x₂)) = x₁
POL(<'(x₁, x₂)) = 0
POL(EQUAL0(x₁, x₂)) = 0
POL(EQUAL0[ITE](x₁, x₂, x₃)) = 0
POL(False) = 0
POL(GCD(x₁, x₂)) = x₁ + x₂
POL(GCD[FALSE][ITE](x₁, x₂, x₃)) = x₁ + x₃
POL(GCD[ITE](x₁, x₂, x₃)) = x₂ + x₃
POL(MONUS(x₁, x₂)) = 0
POL(S(x₁)) = x₁
POL(True) = [1]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁, x₂)) = x₁ + x₂
POL(equal0(x₁, x₂)) = 0
POL(equal0[Ite](x₁, x₂, x₃)) = 0
POL(equal0[True][Ite](x₁, x₂, x₃)) = 0
POL(monus(x₁, x₂)) = 0

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True
monus(S(z0), S(z1)) → monus(z0, z1)

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

S tuples:

GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))

Defined Rule Symbols:

equal0, equal0[Ite], <, equal0[True][Ite], monus

Defined Pair Symbols:

MONUS, GCD, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0

Compound Symbols:

c, c1, c3, c6, c8, c9, c11, c4

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

<'(S(z0), S(z1)) → c3(<'(z0, z1))

We considered the (Usable) Rules:

monus(S(z0), S(z1)) → monus(z0, z1)

And the Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(<(x₁, x₂)) = 0
POL(<'(x₁, x₂)) = x₁·x₂
POL(EQUAL0(x₁, x₂)) = x₁·x₂
POL(EQUAL0[ITE](x₁, x₂, x₃)) = x₂·x₃
POL(False) = 0
POL(GCD(x₁, x₂)) = [2]x₁·x₂
POL(GCD[FALSE][ITE](x₁, x₂, x₃)) = 0
POL(GCD[ITE](x₁, x₂, x₃)) = x₂·x₃
POL(MONUS(x₁, x₂)) = 0
POL(S(x₁)) = [1] + x₁
POL(True) = 0
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁, x₂)) = x₁ + x₂
POL(equal0(x₁, x₂)) = [2]x₂² + x₁·x₂
POL(equal0[Ite](x₁, x₂, x₃)) = [1] + [2]x₂ + [2]x₃ + [2]x₂·x₃ + x₁·x₃ + [2]x₁·x₂
POL(equal0[True][Ite](x₁, x₂, x₃)) = [2]x₁ + [2]x₂ + x₃ + x₃² + x₁·x₃ + [2]x₁² + x₂²
POL(monus(x₁, x₂)) = 0

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True
monus(S(z0), S(z1)) → monus(z0, z1)

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

S tuples:

GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))

Defined Rule Symbols:

equal0, equal0[Ite], <, equal0[True][Ite], monus

Defined Pair Symbols:

MONUS, GCD, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0

Compound Symbols:

c, c1, c3, c6, c8, c9, c11, c4

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace GCD(z0, z1) → c1(GCD[ITE](equal0(z0, z1), z0, z1), EQUAL0(z0, z1)) by

GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True
monus(S(z0), S(z1)) → monus(z0, z1)

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))

S tuples:

GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))

Defined Rule Symbols:

equal0, equal0[Ite], <, equal0[True][Ite], monus

Defined Pair Symbols:

MONUS, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0, GCD

Compound Symbols:

c, c3, c6, c8, c9, c11, c4, c1

(23) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

equal0(z0, z1) → equal0[Ite](<(z0, z1), z0, z1)

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))

S tuples:

GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))

Defined Rule Symbols:

<, monus, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

MONUS, <', GCD[ITE], GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0, GCD

Compound Symbols:

c, c3, c6, c8, c9, c11, c4, c1

(25) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace GCD[ITE](False, z0, z1) → c6(GCD[FALSE][ITE](<(z0, z1), z0, z1), <'(z0, z1)) by

GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)), <'(0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0), <'(z0, 0))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)), <'(0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0), <'(z0, 0))

S tuples:

GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)), <'(0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0), <'(z0, 0))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))

Defined Rule Symbols:

<, monus, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

MONUS, <', GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0, GCD, GCD[ITE]

Compound Symbols:

c, c3, c8, c9, c11, c4, c1, c6

(27) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

S tuples:

GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))

Defined Rule Symbols:

<, monus, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

MONUS, <', GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0, GCD, GCD[ITE]

Compound Symbols:

c, c3, c8, c9, c11, c4, c1, c6, c6

(29) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))

We considered the (Usable) Rules:

monus(S(z0), S(z1)) → monus(z0, z1)

And the Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(<(x₁, x₂)) = 0
POL(<'(x₁, x₂)) = 0
POL(EQUAL0(x₁, x₂)) = 0
POL(EQUAL0[ITE](x₁, x₂, x₃)) = 0
POL(False) = 0
POL(GCD(x₁, x₂)) = x₁ + x₂
POL(GCD[FALSE][ITE](x₁, x₂, x₃)) = x₃
POL(GCD[ITE](x₁, x₂, x₃)) = x₂ + x₃
POL(MONUS(x₁, x₂)) = 0
POL(S(x₁)) = 0
POL(True) = 0
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁, x₂)) = x₁ + x₂
POL(equal0[Ite](x₁, x₂, x₃)) = 0
POL(equal0[True][Ite](x₁, x₂, x₃)) = 0
POL(monus(x₁, x₂)) = 0

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

S tuples:

GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))

Defined Rule Symbols:

<, monus, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

MONUS, <', GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0, GCD, GCD[ITE]

Compound Symbols:

c, c3, c8, c9, c11, c4, c1, c6, c6

(31) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))

We considered the (Usable) Rules:

monus(S(z0), S(z1)) → monus(z0, z1)

And the Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(<(x₁, x₂)) = 0
POL(<'(x₁, x₂)) = 0
POL(EQUAL0(x₁, x₂)) = 0
POL(EQUAL0[ITE](x₁, x₂, x₃)) = 0
POL(False) = 0
POL(GCD(x₁, x₂)) = x₁ + x₂
POL(GCD[FALSE][ITE](x₁, x₂, x₃)) = x₃
POL(GCD[ITE](x₁, x₂, x₃)) = x₂ + x₃
POL(MONUS(x₁, x₂)) = 0
POL(S(x₁)) = [1]
POL(True) = 0
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁, x₂)) = x₁ + x₂
POL(equal0[Ite](x₁, x₂, x₃)) = [1]
POL(equal0[True][Ite](x₁, x₂, x₃)) = 0
POL(monus(x₁, x₂)) = 0

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

S tuples:

GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))

Defined Rule Symbols:

<, monus, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

MONUS, <', GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0, GCD, GCD[ITE]

Compound Symbols:

c, c3, c8, c9, c11, c4, c1, c6, c6

(33) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))

We considered the (Usable) Rules:

monus(S(z0), S(z1)) → monus(z0, z1)
<(z0, 0) → False
<(0, S(z0)) → True
<(S(z0), S(z1)) → <(z0, z1)

And the Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [2]
POL(<(x₁, x₂)) = [1]
POL(<'(x₁, x₂)) = 0
POL(EQUAL0(x₁, x₂)) = [1]
POL(EQUAL0[ITE](x₁, x₂, x₃)) = 0
POL(False) = 0
POL(GCD(x₁, x₂)) = [2] + x₂ + [2]x₁·x₂
POL(GCD[FALSE][ITE](x₁, x₂, x₃)) = [2] + x₁·x₃
POL(GCD[ITE](x₁, x₂, x₃)) = x₃ + [2]x₂·x₃
POL(MONUS(x₁, x₂)) = 0
POL(S(x₁)) = [1]
POL(True) = [1]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁, x₂)) = x₁ + x₂
POL(equal0[Ite](x₁, x₂, x₃)) = [2]x₂·x₃ + [2]x₂²
POL(equal0[True][Ite](x₁, x₂, x₃)) = [2] + [2]x₂ + [2]x₃ + x₃² + [2]x₁·x₃ + x₁·x₂ + x₂²
POL(monus(x₁, x₂)) = 0

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
monus(S(z0), S(z1)) → monus(z0, z1)
equal0[Ite](False, z0, z1) → False
equal0[Ite](True, z0, z1) → equal0[True][Ite](<(z1, z0), z0, z1)
equal0[True][Ite](False, z0, z1) → False
equal0[True][Ite](True, z0, z1) → True

Tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

S tuples:

GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))

K tuples:

MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))
EQUAL0[ITE](True, z0, z1) → c11(<'(z1, z0))
GCD[FALSE][ITE](True, z0, z1) → c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
<'(S(z0), S(z1)) → c3(<'(z0, z1))
GCD[ITE](False, 0, S(z0)) → c6(GCD[FALSE][ITE](True, 0, S(z0)))
GCD[ITE](False, S(z0), S(z1)) → c6(GCD[FALSE][ITE](<(z0, z1), S(z0), S(z1)), <'(S(z0), S(z1)))
EQUAL0(z0, z1) → c4(EQUAL0[ITE](<(z0, z1), z0, z1))
EQUAL0(z0, z1) → c4(<'(z0, z1))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))

Defined Rule Symbols:

<, monus, equal0[Ite], equal0[True][Ite]

Defined Pair Symbols:

MONUS, <', GCD[FALSE][ITE], EQUAL0[ITE], EQUAL0, GCD, GCD[ITE]

Compound Symbols:

c, c3, c8, c9, c11, c4, c1, c6, c6

(35) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

GCD[ITE](False, z0, 0) → c6(GCD[FALSE][ITE](False, z0, 0))
GCD[FALSE][ITE](False, z0, z1) → c8(GCD(z1, monus(z1, z0)), MONUS(z1, z0))
GCD(z0, z1) → c1(GCD[ITE](equal0[Ite](<(z0, z1), z0, z1), z0, z1), EQUAL0(z0, z1))
MONUS(S(z0), S(z1)) → c(MONUS(z0, z1))

Now S is empty

(0) Obligation:

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

(2) Obligation:

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) CdtUsableRulesProof (EQUIVALENT transformation)

(12) Obligation:

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(14) Obligation:

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(16) Obligation:

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(18) Obligation:

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(20) Obligation:

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(22) Obligation:

(23) CdtUsableRulesProof (EQUIVALENT transformation)

(24) Obligation:

(25) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(26) Obligation:

(27) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(28) Obligation:

(29) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(30) Obligation:

(31) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(32) Obligation:

(33) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(34) Obligation:

(35) CdtKnowledgeProof (EQUIVALENT transformation)

(36) BOUNDS(1, 1)